COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00004 00003	#. We will say that a list u is "intermittently contained" in
C00005 00004	#. %2iscompact x%1, where %2x%1 is a list structure, is true if all
C00006 00005	#. %2partitions n%1 is a list of the partitions of the integer %2n%1 into
C00007 00006	# Pattern matching and substitution
C00009 00007	#. Let %2e%1 be a LISP expression formed from numbers and atoms using
C00010 00008	#. Derived functions
C00012 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source
.turn on "→"
CS206∂(30)FINAL EXAMINATION→FALL 1983
.turn off "→"

	This examination is open book and notes.
Write LISP functions or predicates and make proofs
 as follows except where something else is
requested.  Either notation may be used.
Be sure to indicate in an emphatic way the logical sentences indicating
what is to be proved and the %AF%*'s of any inductions that need to be
made.  You may assume that your functions are total but will be
suitably penalized if they aren't.

	The examination is a "take home" and is due at 1983 December 13
Tuesday 7pm in Room 353 Margaret Jacks Hall.  It may also be left
earlier with Diana Hall in Room 358 Margaret Jacks Hall.
.item←0


#. We will say that a list ⊗u is "intermittently contained" in
a list ⊗v if the elements of ⊗u occur in ⊗v in the same order
as in ⊗u but possibly separated by other elements of ⊗v.  We write
%2u_≤≤_v%1 for this relation.  Thus we have  (A_C_E)_≤≤_(X_A_B_C_A_F_D_E_G).

	a. Write a recursive definition of %2u ≤≤ v%1.

Prove

	b. that your %2u ≤≤ v%1 is total

	c. %2∀u:u << u%1.

	d. %2∀u v w:(u ≤≤ v ∧ v ≤≤ w ⊃ u ≤≤ w)%1.

#. %2iscompact x%1, where %2x%1 is a list structure, is true if all
EQUAL substructures in %2x%1 are EQ.

%2compactify x%1 makes a copy of ⊗x that satisfies %2iscompact%1.

What problem arises in trying to prove the properties of %2iscompact%1
by the methods discussed in CS206?

#. %2partitions n%1 is a list of the partitions of the integer %2n%1 into
sums of smaller integers.  Thus
%2partitions_1_=_((1)),
partitions_2_=_((2)_(1_1)),
%2partitions 3 = ((3)_(2_1)_(1_1_1)), and
%2partitions_4_= ((4) (3 1) (2 2) (2 1 1) (1 1 1 1))%1.
# Pattern matching and substitution

	%2sublis[pattern, alist]%1 is the result of making the
substitutions described in ⊗alist in ⊗pattern.  Thus

%2sublis%1[(PLUS X (TIMES X Y) A), ((X.A) (Y.(PLUS X Y)))] 
		= (PLUS A (TIMES A (PLUS X Y)) A)

%2match[pattern,expression,alist]%1 attempts to match ⊗pattern against
⊗expression to produce and extension of ⊗alist such that substituting
in the pattern according to the result will give back %2expression%1.
If the match is unsuccessful, the value is the atom NO.  It is assumed
that a predicate  ⊗isvar  applicable to atoms is available that distinguishes
variables from other atoms.  Assuming that ⊗X and ⊗Y are variables, we have

%2match%1[(PLUS X Y), (PLUS A (TIMES B C)),qnil] = ((X.A) (Y TIMES B C)),

and

%2match%1[(PLUS X Y), (PLUS A (TIMES B C)),((X.B))] = NO.

a. Write recursive programs for ⊗sublis and ⊗match. 

b. Write accurately the sentence that expresses the fact that
⊗sublis and ⊗match are partial inverses.

c. Prove the sentence of part b.

#. Let %2e%1 be a LISP expression formed from numbers and atoms using
PLUS and TIMES to represent addition and multiplication.  %2polyprint_e%1
is a list of the characters occurring in a printout of %2e%1 in
algebraic notation containing no unnecessary parentheses.  Thus

	%2polyprint%1 (TIMES (PLUS X (TIMES U V W)) X Z) =
(LP X PLUS U V W RP X Z)

which corresponds to the algebraic expression (X + UVW)XZ

#. Derived functions

	Certain properties of LISP functions are expressed by related
functions called derived functions.  For example, consider

%2flatten x ← qif qat x qthen <x> qelse flatten qa x * flatten qd x%1.

Let %2cflatten x%1 be the number of times LISP executes ⊗cons in
evaluating %2flatten x%1.  Clearly ⊗cflatten satisfies the recursions

%2cflatten x ← qif qat x qthen 1
	qelse cflatten qa x + cflatten qd x + cappend[flatten qa x, flatten qd x]%1,

where ⊗cappend[u,v] is the number of conses done in computing %2u*v%1
and satisfies

%2cappend[u,v] ← qif qn u then 0 qelse 1 + cappend[qd u, v]%1.

	Our other way of flattening a list involves

%2flat[x,u] ← qif qat x qthen x.u qelse flat[qa x, flat[qd x, u]]%1.

Let ⊗cflat[x,u] be the number of %2cons%1es done in computing %2flat[x,u]%1.

	a. Write the recursion for %2cflat[x,u]%1.

	b. Prove %2∀x u: cflat[x,u] ≤ cflatten x%1.